\chapter{Type Soundness Proof}
\section{Introduction}
The extent to which a programming language restricts the syntax so as to prevent type errors is called type safety. Robin Milner correctly stated type safety as "Well typed programs cannot go wrong!''. The type safety property ensures that the execution of a well typed program will result in an expected type. A correctly compiled program cannot break at runtime due to type error.\\
JavaPict is an extension to Java, which adds two new notions, of processes and channels. Processes are entities which holds ports wherein the channels are attached. Channels are synchronous objects through which processes send and receive messages from other connected processes. For simplicity, we model mobile channels i.e. sending channels over channels by allowing a process to change its connections from one channel to another.\\
This part of the thesis proves that JavaPict is type sound. Formally we use Featherweight generic Java and extend it to include channels and processes and prove the type soundness of the new system.
\section{Featherweight Generic Java (FGJ)}
\subsection{Background}
Featherweight generic java \cite{FGJ} or FGJ is a minimal core calculus for modelling Java's type system. FGJ is designed, giving more importance to compactness than to completeness. The syntax consists of minimal number of expressions making extension an easier task. FGJ term can be of a type or of a variable type as mentioned in figure 1. There are only five forms of expressions in FJ(Featherweight Java) namely, object creation, method invocation, field access, casting, and variables. In FGJ this syntax is extended to include generic types for all these expressions. FGJ was designed solely to model the complex Java type system with minimal constructs which can be extended to include vital expressions.
\subsection{FGJ definitions}
A java program consists of class definitions and an expression. Formally, a Java program is a pair of class table (CT) and an expression i.e. (CT, e). A class table is a mapping from class names C to class declarations L. Certain restrictions are imposed in order to maintain syntactic regularity. 
\begin{itemize}
\item Class(class C extends B \{${\overline C}$ ${\overline f}$;  K ${\overline M}$\})
  \begin{itemize}
    \item Every class has a superclass i.e the definition should include an {\it extends} clause i.e class C extends D \{...\} (In trivial case, the superclass is {\it Object})
    \item The class {\it Object} is not included in the class table(So as to maintain the previous restriction)
    \item A class always contains one constructor(K) with number of arguments equal to the sum of number of its own fields and the number of fields in superclass. 
    \item All fields are public and final 
    \item Class contains methods denoted by ${\overline M}$
  \end{itemize}
\item Method
  \begin{itemize}
    \item A method header contains a return type, a method name and arguments  
    \item Method includes only a single expression containing a return statement
  \end{itemize}
\end{itemize}
% Consider the following example:
% \begin{verbatim}
% class Key extends Object{
%     Key(){super();}
% }
% 
% class Value extends Object{
%     Value(){super();}
% }
% 
% class Pair<X extends Object, Y extends Object> extends Object{
%     X first;
%     Y second;
%     Pair(X first, Y second){
%         super();
%         this.first = first; 
%         this.second = second;
%     }
%     <Z extends Object> Pair<Z, Y> setfirst(Z newfirst){
%         return new Pair<Z, Y>(newfirst, this.second);
%     }
% }
% \end{verbatim}
% Class and method could include generic types. Here X and Y are generic type of class and Z is a parameter of the method setfirst. Generic type is also called a variable type. Each variable type parameter is bounded on the upper side; here X Y and Z are all bounded by Object. The bound need not necessarily be a type variable, it could also be an expression involving type variables. Thus the type variables could include recursive as well as circular bounds. For example, $<$X extends C$<$X$>$ $>$ or $<$X extends C$<$Y$>$, Y extends C$<$X$>$ $>$.\\
Generic Java i.e extension of java with generics uses type erasure for implementation. Type erasure ensures that the java compiler compiles GJ into Java Virtual Machine(JVM), erasing all mention of generic type variables and extracting all information from the provided code at runtime. 
\subsection{Syntax for FGJ}
\begin{table}
\begin{tabular}{|p{\linewidth}|}
\hline
T := X$|$N \\
N := C$<{\overline T}>$ \\
L := class C$<{\overline X}\triangleleft{\overline N}>$ $\triangleleft$ N \{${\overline T}$ ${\overline f}$; K ${\overline M}$\} \\
K := C(${\overline T}$ ${\overline f}$) \{ super(${\overline f}$); this.${\overline f}$ = ${\overline f}$;\}\\
M := $<{\overline X}$ $\triangleleft$ ${\overline N}>$ T m(${\overline T}$ ${\overline x}$)\{ return e; \}\\
e := x $|$ e.f $|$ e.m$<{\overline T}>$(${\overline e}$) $|$ new N(${\overline e}$) $|$ (N)e \\
\hline
\end{tabular}
\caption{Syntax}
\end{table}
The syntax of FGJ is described in Table 5.1. This notation is followed throughout this paper. The type X$_1$, X$_2$... X$_n$ is denoted by ${\overline X}$. Similarly field declaration or parameters T$_1$ f$_1$; T$_2$ f$_2$ ....T$_n$ f$_n$ is denoted by ${\overline T}$ ${\overline f}$. The keywords extends is replaced by the symbol $\triangleleft$. X, Y and Z denotes the type variables and N, M, P and Q range over the types. K is reserved for the constructor of a class.\\
 Method declaration has a return type and header which binds the generic types like $<{\overline X}$ $\triangleleft$ ${\overline N}>$. A class can contain one or more such methods. An expression could be a variable reference, a field access, method call, object creation or type cast. The subclass relation is denoted by $\unlhd$. Thus if C is a subclass of D then this relation is denoted by C $\unlhd$ D.    
\cite{FGJ} provides a rigorous proof for type soundness of FGJ.\\
% \subsection{Auxillary functions} 
% \begin{table}
% \begin{tabular}{|p{\linewidth}|}
% \hline\\
% {\bf Subclass} \\
% \begin{center}{\large $\frac {C\ \unlhd\ D\ \  D\ \unlhd\ E}{C\ \unlhd\ E}$} \end{center}\\
% \hline\\
% {\bf Fields}\\
% \begin{center} {\large $\frac {class\ C<\overline X\ \triangleleft\ \overline N>\ \triangleleft\  N \{\  \overline T \ \overline f;\ K \ \overline M\}} {fields(C)\ =\ \overline T \ \overline f}$} \end{center}\\
% \hline\\
% \vspace{-18pt}
% {\bf Method functions}\\
% \hline\\
% \begin{center}
%  $\dfrac 
%   {
%     \splitfrac{class\ C<\overline X\ \triangleleft\ \overline N>\ \triangleleft\  N \{\  \overline T \ \overline f;\ K \ \overline M\}} 
%               {<\overline X\ \triangleleft\ \overline N>\ T\ m(\overline T\ \overline x)\{\ return\ e;\ \} \ \ m \in \overline M}
%   }
%   {mtype(m,\ C)\ =\ <\overline X\ \triangleleft\ \overline N>\ \rightarrow\ T}$
% \end{center}\\
% \hline
% \end{tabular}
% \caption{Auxillary functions}
% \end{table}
% The functions defined in Table 5.2 will be helpful to modularize the proof and make it readeable. The fields of a class C are given by fields(C), which is a sequence of types and field names, ${\overline T}$ ${\overline f}$. The method mtype(m, C$<{\overline T}>$) denotes the type declaration of the method m in class C$<{\overline T}>$. For eg. in the syntax defined in table 5.1 mtype(m, C) will be $<{\overline X}$ $\triangleleft$ ${\overline N}> \rightarrow$  T. The function mbody(m, C$<{\overline T}>$) is a expression specifying the parameters and the return value of the method i.e. ${\overline x}$.e. 